A:Type, f:(A), L:A List, a:A.
(a  L)  f(a)  (b:A. a before b  L  f(b))  (a  2of(split_tail(L | x.f(x)))) 

latex

Definitions	b, t  T, x:A. B(x), , ||as||, P  Q, False, A, AB, , l[i], Prop, A & B, x:A. B(x), x(s), x before y  l, (x  l), P  Q, P & Q, P  Q, split_tail(L | x.f(x)), x. t(x), P  Q, True, b, Unit, {T}, SQType(T), if b t else f fi, 2of(t)
Lemmas	split tail wf, pi2 wf, ifthenelse wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, cons before, split tail trivial, cons member, l member wf, l before wf, assert wf, nat wf, select wf, length wf2, bool wf